Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    O(0)  → 0
2:    0 + x  → x
3:    x + 0  → x
4:    O(x) + O(y)  → O(x + y)
5:    O(x) + I(y)  → I(x + y)
6:    I(x) + O(y)  → I(x + y)
7:    I(x) + I(y)  → O((x + y) + I(0))
8:    x + (y + z)  → (x + y) + z
9:    x - 0  → x
10:    0 - x  → 0
11:    O(x) - O(y)  → O(x - y)
12:    O(x) - I(y)  → I((x - y) - I(1))
13:    I(x) - O(y)  → I(x - y)
14:    I(x) - I(y)  → O(x - y)
15:    not(true)  → false
16:    not(false)  → true
17:    and(x,true)  → x
18:    and(x,false)  → false
19:    if(true,x,y)  → x
20:    if(false,x,y)  → y
21:    ge(O(x),O(y))  → ge(x,y)
22:    ge(O(x),I(y))  → not(ge(y,x))
23:    ge(I(x),O(y))  → ge(x,y)
24:    ge(I(x),I(y))  → ge(x,y)
25:    ge(x,0)  → true
26:    ge(0,O(x))  → ge(0,x)
27:    ge(0,I(x))  → false
28:    Log'(0)  → 0
29:    Log'(I(x))  → Log'(x) + I(0)
30:    Log'(O(x))  → if(ge(x,I(0)),Log'(x) + I(0),0)
31:    Log(x)  → Log'(x) - I(0)
32:    Val(L(x))  → x
33:    Val(N(x,l,r))  → x
34:    Min(L(x))  → x
35:    Min(N(x,l,r))  → Min(l)
36:    Max(L(x))  → x
37:    Max(N(x,l,r))  → Max(r)
38:    BS(L(x))  → true
39:    BS(N(x,l,r))  → and(and(ge(x,Max(l)),ge(Min(r),x)),and(BS(l),BS(r)))
40:    Size(L(x))  → I(0)
41:    Size(N(x,l,r))  → (Size(l) + Size(r)) + I(1)
42:    WB(L(x))  → true
43:    WB(N(x,l,r))  → and(if(ge(Size(l),Size(r)),ge(I(0),Size(l) - Size(r)),ge(I(0),Size(r) - Size(l))),and(WB(l),WB(r)))
There are 57 dependency pairs:
44:    O(x) +# O(y)  → O#(x + y)
45:    O(x) +# O(y)  → x +# y
46:    O(x) +# I(y)  → x +# y
47:    I(x) +# O(y)  → x +# y
48:    I(x) +# I(y)  → O#((x + y) + I(0))
49:    I(x) +# I(y)  → (x + y) +# I(0)
50:    I(x) +# I(y)  → x +# y
51:    x +# (y + z)  → (x + y) +# z
52:    x +# (y + z)  → x +# y
53:    O(x) -# O(y)  → O#(x - y)
54:    O(x) -# O(y)  → x -# y
55:    O(x) -# I(y)  → (x - y) -# I(1)
56:    O(x) -# I(y)  → x -# y
57:    I(x) -# O(y)  → x -# y
58:    I(x) -# I(y)  → O#(x - y)
59:    I(x) -# I(y)  → x -# y
60:    GE(O(x),O(y))  → GE(x,y)
61:    GE(O(x),I(y))  → NOT(ge(y,x))
62:    GE(O(x),I(y))  → GE(y,x)
63:    GE(I(x),O(y))  → GE(x,y)
64:    GE(I(x),I(y))  → GE(x,y)
65:    GE(0,O(x))  → GE(0,x)
66:    Log'#(I(x))  → Log'(x) +# I(0)
67:    Log'#(I(x))  → Log'#(x)
68:    Log'#(O(x))  → IF(ge(x,I(0)),Log'(x) + I(0),0)
69:    Log'#(O(x))  → GE(x,I(0))
70:    Log'#(O(x))  → Log'(x) +# I(0)
71:    Log'#(O(x))  → Log'#(x)
72:    Log#(x)  → Log'(x) -# I(0)
73:    Log#(x)  → Log'#(x)
74:    Min#(N(x,l,r))  → Min#(l)
75:    Max#(N(x,l,r))  → Max#(r)
76:    BS#(N(x,l,r))  → AND(and(ge(x,Max(l)),ge(Min(r),x)),and(BS(l),BS(r)))
77:    BS#(N(x,l,r))  → AND(ge(x,Max(l)),ge(Min(r),x))
78:    BS#(N(x,l,r))  → GE(x,Max(l))
79:    BS#(N(x,l,r))  → Max#(l)
80:    BS#(N(x,l,r))  → GE(Min(r),x)
81:    BS#(N(x,l,r))  → Min#(r)
82:    BS#(N(x,l,r))  → AND(BS(l),BS(r))
83:    BS#(N(x,l,r))  → BS#(l)
84:    BS#(N(x,l,r))  → BS#(r)
85:    Size#(N(x,l,r))  → (Size(l) + Size(r)) +# I(1)
86:    Size#(N(x,l,r))  → Size(l) +# Size(r)
87:    Size#(N(x,l,r))  → Size#(l)
88:    Size#(N(x,l,r))  → Size#(r)
89:    WB#(N(x,l,r))  → AND(if(ge(Size(l),Size(r)),ge(I(0),Size(l) - Size(r)),ge(I(0),Size(r) - Size(l))),and(WB(l),WB(r)))
90:    WB#(N(x,l,r))  → IF(ge(Size(l),Size(r)),ge(I(0),Size(l) - Size(r)),ge(I(0),Size(r) - Size(l)))
91:    WB#(N(x,l,r))  → GE(Size(l),Size(r))
92:    WB#(N(x,l,r))  → GE(I(0),Size(l) - Size(r))
93:    WB#(N(x,l,r))  → Size(l) -# Size(r)
94:    WB#(N(x,l,r))  → GE(I(0),Size(r) - Size(l))
95:    WB#(N(x,l,r))  → Size(r) -# Size(l)
96:    WB#(N(x,l,r))  → Size#(r)
97:    WB#(N(x,l,r))  → Size#(l)
98:    WB#(N(x,l,r))  → AND(WB(l),WB(r))
99:    WB#(N(x,l,r))  → WB#(l)
100:    WB#(N(x,l,r))  → WB#(r)
The approximated dependency graph contains 5 SCCs: {65}, {45-47,49-52}, {54-57,59}, {60,62-64} and {67,71}.
Tyrolean Termination Tool  (0.15 seconds)   ---  May 4, 2006